'Weak Dependency Graph [60.0]' ------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { c(c(c(y))) -> c(c(a(y, 0()))) , c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c(y) -> y} Details: We have computed the following set of weak (innermost) dependency pairs: { c^#(c(c(y))) -> c_0(c^#(c(a(y, 0())))) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0())))) , c^#(y) -> c_2()} The usable rules are: { c(c(c(y))) -> c(c(a(y, 0()))) , c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c(y) -> y} The estimated dependency graph contains the following edges: {c^#(c(c(y))) -> c_0(c^#(c(a(y, 0()))))} ==> {c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} {c^#(c(c(y))) -> c_0(c^#(c(a(y, 0()))))} ==> {c^#(y) -> c_2()} {c^#(c(c(y))) -> c_0(c^#(c(a(y, 0()))))} ==> {c^#(c(c(y))) -> c_0(c^#(c(a(y, 0()))))} {c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} ==> {c^#(y) -> c_2()} {c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} ==> {c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} {c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} ==> {c^#(c(c(y))) -> c_0(c^#(c(a(y, 0()))))} We consider the following path(s): 1) { c^#(c(c(y))) -> c_0(c^#(c(a(y, 0())))) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0())))) , c^#(y) -> c_2()} The usable rules for this path are the following: { c(c(c(y))) -> c(c(a(y, 0()))) , c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c(y) -> y} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { c(c(c(y))) -> c(c(a(y, 0()))) , c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c(y) -> y , c^#(c(c(y))) -> c_0(c^#(c(a(y, 0())))) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0())))) , c^#(y) -> c_2()} Details: We apply the weight gap principle, strictly orienting the rules {c^#(y) -> c_2()} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {c^#(y) -> c_2()} Details: Interpretation Functions: c(x1) = [1] x1 + [0] a(x1, x2) = [1] x1 + [1] x2 + [0] 0() = [0] c^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [0] c_2() = [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} and weakly orienting the rules {c^#(y) -> c_2()} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} Details: Interpretation Functions: c(x1) = [1] x1 + [0] a(x1, x2) = [1] x1 + [1] x2 + [8] 0() = [0] c^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [8] c_1(x1) = [1] x1 + [9] c_2() = [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {c(y) -> y} and weakly orienting the rules { c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0())))) , c^#(y) -> c_2()} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {c(y) -> y} Details: Interpretation Functions: c(x1) = [1] x1 + [1] a(x1, x2) = [1] x1 + [1] x2 + [2] 0() = [0] c^#(x1) = [1] x1 + [2] c_0(x1) = [1] x1 + [2] c_1(x1) = [1] x1 + [0] c_2() = [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { c(c(c(y))) -> c(c(a(y, 0()))) , c^#(c(c(y))) -> c_0(c^#(c(a(y, 0()))))} Weak Rules: { c(y) -> y , c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0())))) , c^#(y) -> c_2()} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { c(c(c(y))) -> c(c(a(y, 0()))) , c^#(c(c(y))) -> c_0(c^#(c(a(y, 0()))))} Weak Rules: { c(y) -> y , c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0())))) , c^#(y) -> c_2()} Details: The problem is Match-bounded by 1. The enriched problem is compatible with the following automaton: { c_0(3) -> 6 , c_0(3) -> 7 , c_0(7) -> 6 , c_1(10) -> 9 , a_0(2, 2) -> 2 , a_0(2, 3) -> 2 , a_0(3, 2) -> 2 , a_0(3, 3) -> 2 , a_1(3, 11) -> 9 , a_1(3, 11) -> 10 , 0_0() -> 3 , 0_0() -> 6 , 0_0() -> 7 , 0_1() -> 11 , c^#_0(2) -> 4 , c^#_0(3) -> 4 , c^#_0(6) -> 5 , c^#_1(9) -> 8 , c_0_1(8) -> 5 , c_1_0(5) -> 4 , c_2_0() -> 4 , c_2_0() -> 5 , c_2_1() -> 8} 2) { c^#(c(c(y))) -> c_0(c^#(c(a(y, 0())))) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} The usable rules for this path are the following: { c(c(c(y))) -> c(c(a(y, 0()))) , c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c(y) -> y} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { c(c(c(y))) -> c(c(a(y, 0()))) , c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c(y) -> y , c^#(c(c(y))) -> c_0(c^#(c(a(y, 0())))) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} Details: We apply the weight gap principle, strictly orienting the rules { c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} Details: Interpretation Functions: c(x1) = [1] x1 + [0] a(x1, x2) = [1] x1 + [1] x2 + [8] 0() = [0] c^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [0] c_2() = [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {c(y) -> y} and weakly orienting the rules { c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {c(y) -> y} Details: Interpretation Functions: c(x1) = [1] x1 + [1] a(x1, x2) = [1] x1 + [1] x2 + [2] 0() = [0] c^#(x1) = [1] x1 + [2] c_0(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [2] c_2() = [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { c(c(c(y))) -> c(c(a(y, 0()))) , c^#(c(c(y))) -> c_0(c^#(c(a(y, 0()))))} Weak Rules: { c(y) -> y , c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { c(c(c(y))) -> c(c(a(y, 0()))) , c^#(c(c(y))) -> c_0(c^#(c(a(y, 0()))))} Weak Rules: { c(y) -> y , c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) , c^#(a(a(0(), x), y)) -> c_1(c^#(c(c(0()))))} Details: The problem is Match-bounded by 1. The enriched problem is compatible with the following automaton: { c_0(3) -> 6 , c_0(3) -> 7 , c_0(7) -> 6 , c_1(10) -> 9 , a_0(2, 2) -> 2 , a_0(2, 3) -> 2 , a_0(3, 2) -> 2 , a_0(3, 3) -> 2 , a_1(3, 11) -> 9 , a_1(3, 11) -> 10 , 0_0() -> 3 , 0_0() -> 6 , 0_0() -> 7 , 0_1() -> 11 , c^#_0(2) -> 4 , c^#_0(3) -> 4 , c^#_0(6) -> 5 , c^#_1(9) -> 8 , c_0_1(8) -> 5 , c_1_0(5) -> 4}